Inference at * 2 2 1 
Iof proof for Lemma p-fun-exp-add-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. m : 
5. 0 < m
6. n:. (can-apply(f^m - 1;x))  ((f^n+(m - 1)(x)) ~ (f^n(do-apply(f^m - 1;x))))
7. n : 
8. can-apply(f^m;x)
9. (n = 0)
10. (n+m = 0)
11. (n = 0)
12. (m = 0)
  (f o f^(n+m) - 1  (x)) ~ (f o f^n - 1  (do-apply(f o f^m - 1  ;x))) 

latex

 by Subst' (f o f^(n+m) - 1  (x)) ~ (f o f^n  (do-apply(f^m - 1;x))) ( 0) 

latex

 1: .....equality..... NILNIL

 1:   (f o f^(n+m) - 1  (x)) ~ (f o f^n  (do-apply(f^m - 1;x)))
 2: 

 2:   (f o f^n  (do-apply(f^m - 1;x))) ~ (f o f^n - 1  (do-apply(f o f^m - 1  ;x)))
 .

Definitions

s ~ t, n+m, f(a), f o g  , do-apply(f;x), f^n, n - m, #$n